Definitions	Feasible(D), , P & Q, x:A. B(x), M(i), t  T, M.dout(l,tg), , M.din(l,tg), f(x)?z, 1of(t), 2of(t), mk-ma, , Top, if b t else f fi, x  dom(f), deq-member(eq;x;L), reduce(f;k;as), false, Y, b, M sends on link l, map(f;as), finite-type(T), False, x:A. B(x), , AB, A, P  Q, Prop, Surj(A; B; f), {i..j}, i  j < k
Lemmas	Id wf, IdLnk wf, ma-empty-feasible, top wf, le wf, int seg wf, surject wf, ldst wf, false wf